A:Type, I:MaInterface(A), l:IdLnk, tg:Id. gluable2(A;I;l;tg)   

latex

Definitions	t  T, Type, x:A  B(x), Id, b, a:A fp B(a), MaInterface(T), IdLnk, P  Q, x:A. B(x), ma-interface-valtype(I;i;k), hasloc(k;i), {x:A| B(x)} , Knd, type List, x:AB(x), S  T, ma-interface-dom(I;i), rcv(l,tg), (x  l), ma-interface-locs(I), destination(l), Atom$n, , gluable2(A;I;l;tg)
Lemmas	ldst wf, ma-interface-locs wf, l member wf, Knd wf, rcv wf, ma-interface-dom wf, assert wf, hasloc wf, subtype rel wf, ma-interface-valtype wf